/*
 * Kodkod -- Copyright (c) 2005-present, Emina Torlak
 *
 * Permission is hereby granted, free of charge, to any person obtaining a copy
 * of this software and associated documentation files (the "Software"), to deal
 * in the Software without restriction, including without limitation the rights
 * to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
 * copies of the Software, and to permit persons to whom the Software is
 * furnished to do so, subject to the following conditions:
 *
 * The above copyright notice and this permission notice shall be included in
 * all copies or substantial portions of the Software.
 *
 * THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
 * IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
 * FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
 * AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
 * LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
 * OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN
 * THE SOFTWARE.
 */
package kodkod.engine;

import java.util.Iterator;
import java.util.Map;

import kodkod.ast.Formula;
import kodkod.ast.Node;
import kodkod.engine.config.Options;
import kodkod.engine.fol2sat.TranslationLog;
import kodkod.engine.fol2sat.TranslationRecord;
import kodkod.engine.satlab.ReductionStrategy;
import kodkod.util.nodes.Nodes;

/**
 * Contains a proof of unsatisfiability of a given FOL formula.
 *
 * @specfield log: TranslationLog // log of the translation of this.formula with
 *            respect to this.bounds
 */
public abstract class Proof {

    private final TranslationLog log;

    /**
     * Constructs a new Proof of unsatisfiability for log.formula.
     *
     * @ensures this.log = log
     */
    Proof(TranslationLog log) {
        this.log = log;
    }

    /**
     * Minimizes the proof of this.log.formula's unsatisfiability using the
     * specified proof reduction strategy. The strategy argument is ignored (it can
     * be null) if this.formula is trivially unsatisfiable with respect to
     * this.bounds. In that case, the core is reduced using the trivial strategy
     * that does one of the following: (1) if there is a root that simplified to
     * FALSE, sets the minimal core to that root; or (2) if not, then there must be
     * two roots that translated to x and -x, where x is a boolean literal, so we
     * pick those two as the minimal core.
     * <p>
     * <b>Note:</b> the core minimization is performed at the level of the
     * transformed formula, not the original formula if the problem was translated
     * with a non-zero {@linkplain Options#coreGranularity() core granularity}
     * setting. In other words, after this method has been called,
     * {@linkplain #highLevelCore() highLevelCore()} returns a map M such that
     * M.keySet() is a minimal core with respect to this.log.bounds. In contrast,
     * {@linkplain Nodes#allRoots(Formula, java.util.Collection)
     * Nodes.roots(this.log.originalFormula, M.values())} is unsatisfiable with
     * respect this.log.originalBounds. These formulas, however, do not necessarily
     * form a minimal core of this.log.originalFormula if the original problem was
     * translated with a non-zero {@linkplain Options#coreGranularity() core
     * granularity} setting.
     * </p>
     *
     * @ensures minimizes the proof of this.log.formula's unsatisfiability using the
     *          specified proof reduction strategy (or the trivial strategy if
     *          this.formula is trivially unsatisfiable with respect to
     *          this.bounds).
     * @see kodkod.engine.satlab.ReductionStrategy
     */
    public abstract void minimize(ReductionStrategy strategy);

    /**
     * Returns an iterator over the {@link TranslationRecord log records} for the
     * nodes that are in the unsatisfiable core of this.log.formula. The record
     * objects returned by the iterator are not guaranteed to be immutable. In
     * particular, the state of a record object returned by <tt>next()</tt> is
     * guaranteed to remain the same only until the subsequent call to
     * <tt>next()</tt>.
     *
     * @return an iterator over the {@link TranslationRecord log records} for the
     *         nodes that are in the unsatisfiable core of this.log.formula.
     */
    public abstract Iterator<TranslationRecord> core();

    /**
     * Returns a map whose key set is the unsatisfiable subset of the top-level
     * conjunctions of this.log.formula as given by {@linkplain #core()
     * this.core()}. Each formula in the key set is mapped to the descendant of
     * this.log.originalFormula from which it was derived by skolemization or by
     * some other optimization.
     *
     * @return a map whose key set is the unsatisfiable subset of the top-level
     *         conjunctions of this.log.formula, as given by {@linkplain #core()
     *         this.core()}. Each formula in the key set is mapped to the descendant
     *         of this.log.originalFormula from which it was derived by
     *         skolemization or by some other optimization.
     * @see #minimize(ReductionStrategy)
     */
    public abstract Map<Formula,Node> highLevelCore();

    /**
     * Returns the log of the translation that resulted in this proof.
     *
     * @return log of the translation that resulted in this proof
     */
    public final TranslationLog log() {
        return log;
    }

    /**
     * Returns a string representation of this proof.
     *
     * @return a string representation of this proof.
     * @see java.lang.Object#toString()
     */
    // public String toString() {
    // final StringBuilder ret = new StringBuilder();
    // for(Formula f : highLevelCore()) {
    // ret.append(" ");
    // ret.append(f);
    // ret.append("\n");
    // }
    // return ret.toString();
    // }

}
